es:ES, ff:FIFO, f2f+:F2F+-decls.
plus-ify{i:l}(es;ff;is_req  ;is_ack ;awaiting ;owes_ack )
 (sndr, rcvr:ff.C.
 single-thread-generator{i:l}(es;e.[e: sndr is_req   rcvr]
  [e: rcvr is_ack  sndr];e,e'. f2f+-pred(e,e'))) 

latex

Definitions	A, R1 => R2, , A c B, x f y, x(s), P  Q, single-thread-generator{i:l}(es;P;R), t  T, P & Q, P  Q, x:A. B(x), False, {T}
Lemmas	f2f+-pred-no-forks, f2f+-pred-at-most-one-min, f2f+-pred-field, f2f+-pred-sub-causl, decidable snd-it, decidable or, not wf, f2f+-pred wf, snd-it wf, decidable f2f+-pred, event system wf, FIFO wf, F2F+-decls wf, fifoS wf, es-E wf, fifoR wf, f2f+Owes wf, f2f+Wait wf, f2f+Ack wf, f2f+Req wf, plus-ify wf, fifoC wf, f2f+-property